es:event_system{i:l}, e,e':es-E(es).
es-locl(es; e; e')  ([e, e'] = append([e, es-pred(es; e')]; cons(e'; []))  (es-E(es) List)) 

latex

Definitions	es-E(es), append(as; bs), filter(P; l), t  T, x:A. B(x), P  Q, P  Q, P  Q, es-pred(es; e), t.1, before(e), es-ble{i:l}(es;e;e'), , [e, e'], event_system{i:l}, es-locl(es; e; e'), b, A, b, prop{i:l}, es-first(es; e), Unit, False, True, T, tt, P  Q, x(s), x. t(x), l_all(L; T; x.P(x)), P  Q, es-le(es; e; e')
Lemmas	assert-es-ble, filter trivial, l all reduce, assert of band, btrue wf, squash wf, true wf, append wf, filter wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, es-locl wf, event system wf, filter append, es-ble wf, es-before wf, es-pred wf, es-locl-iff, es-E wf